Left Termination proof of /tmp/tmpv6Wsun/pl5.2.2.pl

Left Termination of the query pattern turing_in_4(g, g, g, a) w.r.t. the given Prolog program could not be shown:

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

Clauses:

member(H, .(H, L)).
member(X, .(H, L)) :- member(X, L).
turing(t(X, Y, Z), S, P, t(X, Y, Z)) :- member(p(S, Y, halt, W, D), P).
turing(t(X, Y, .(R, L)), S, P, T) :- ','(member(p(S, Y, S1, W, r), P), turing(t(.(W, X), R, L), S1, P, T)).
turing(t(X, Y, []), S, P, T) :- ','(member(p(S, Y, S1, W, r), P), turing(t(.(W, X), space, []), S1, P, T)).
turing(t(.(X, L), Y, R), S, P, T) :- ','(member(p(S, Y, S1, W, l), P), turing(t(L, X, .(W, R)), S1, P, T)).
turing(t([], Y, R), S, P, T) :- ','(member(p(S, Y, S1, W, l), P), turing(t([], space, .(W, R)), S1, P, T)).

Queries:

turing(g,g,g,a).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
turing_in: (b,b,b,f) (b,f,b,f)
member_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

turing_in_ggga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_ggga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U2_ggga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_ggga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_ggga(t(X, Y, .(R, L)), S, P, T) → U3_ggga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_ggga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_ggga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_gaga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
U2_gaga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_gaga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_gaga(t(X, Y, .(R, L)), S, P, T) → U3_gaga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_gaga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_gaga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, []), S, P, T) → U5_gaga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_gaga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_gaga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
turing_in_gaga(t(.(X, L), Y, R), S, P, T) → U7_gaga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_gaga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_gaga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
turing_in_gaga(t([], Y, R), S, P, T) → U9_gaga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_gaga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_gaga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_gaga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_gaga(t([], Y, R), S, P, T)
U8_gaga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_gaga(t(.(X, L), Y, R), S, P, T)
U6_gaga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_gaga(t(X, Y, []), S, P, T)
U4_gaga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_gaga(t(X, Y, .(R, L)), S, P, T)
U4_ggga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_ggga(t(X, Y, .(R, L)), S, P, T)
turing_in_ggga(t(X, Y, []), S, P, T) → U5_ggga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_ggga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_ggga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U6_ggga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_ggga(t(X, Y, []), S, P, T)
turing_in_ggga(t(.(X, L), Y, R), S, P, T) → U7_ggga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_ggga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_ggga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U8_ggga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_ggga(t(.(X, L), Y, R), S, P, T)
turing_in_ggga(t([], Y, R), S, P, T) → U9_ggga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_ggga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_ggga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_ggga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_ggga(t([], Y, R), S, P, T)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

turing_in_ggga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_ggga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U2_ggga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_ggga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_ggga(t(X, Y, .(R, L)), S, P, T) → U3_ggga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_ggga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_ggga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_gaga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
U2_gaga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_gaga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_gaga(t(X, Y, .(R, L)), S, P, T) → U3_gaga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_gaga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_gaga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, []), S, P, T) → U5_gaga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_gaga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_gaga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
turing_in_gaga(t(.(X, L), Y, R), S, P, T) → U7_gaga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_gaga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_gaga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
turing_in_gaga(t([], Y, R), S, P, T) → U9_gaga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_gaga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_gaga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_gaga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_gaga(t([], Y, R), S, P, T)
U8_gaga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_gaga(t(.(X, L), Y, R), S, P, T)
U6_gaga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_gaga(t(X, Y, []), S, P, T)
U4_gaga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_gaga(t(X, Y, .(R, L)), S, P, T)
U4_ggga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_ggga(t(X, Y, .(R, L)), S, P, T)
turing_in_ggga(t(X, Y, []), S, P, T) → U5_ggga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_ggga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_ggga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U6_ggga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_ggga(t(X, Y, []), S, P, T)
turing_in_ggga(t(.(X, L), Y, R), S, P, T) → U7_ggga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_ggga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_ggga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U8_ggga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_ggga(t(.(X, L), Y, R), S, P, T)
turing_in_ggga(t([], Y, R), S, P, T) → U9_ggga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_ggga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_ggga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_ggga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_ggga(t([], Y, R), S, P, T)

TURING_IN_GGGA(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_GGGA(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
TURING_IN_GGGA(t(X, Y, Z), S, P, t(X, Y, Z)) → MEMBER_IN_GG(p(S, Y, halt, W, D), P)
MEMBER_IN_GG(X, .(H, L)) → U1_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
TURING_IN_GGGA(t(X, Y, .(R, L)), S, P, T) → U3_GGGA(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GGGA(t(X, Y, .(R, L)), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U3_GGGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_GGGA(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
U3_GGGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), R, L), S1, P, T)
TURING_IN_GAGA(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_GAGA(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
TURING_IN_GAGA(t(X, Y, Z), S, P, t(X, Y, Z)) → MEMBER_IN_GG(p(S, Y, halt, W, D), P)
TURING_IN_GAGA(t(X, Y, .(R, L)), S, P, T) → U3_GAGA(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GAGA(t(X, Y, .(R, L)), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U3_GAGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_GAGA(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
U3_GAGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), R, L), S1, P, T)
TURING_IN_GAGA(t(X, Y, []), S, P, T) → U5_GAGA(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GAGA(t(X, Y, []), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U5_GAGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_GAGA(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U5_GAGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), space, []), S1, P, T)
TURING_IN_GAGA(t(.(X, L), Y, R), S, P, T) → U7_GAGA(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GAGA(t(.(X, L), Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U7_GAGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_GAGA(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U7_GAGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t(L, X, .(W, R)), S1, P, T)
TURING_IN_GAGA(t([], Y, R), S, P, T) → U9_GAGA(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GAGA(t([], Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U9_GAGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_GAGA(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U9_GAGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t([], space, .(W, R)), S1, P, T)
TURING_IN_GGGA(t(X, Y, []), S, P, T) → U5_GGGA(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GGGA(t(X, Y, []), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U5_GGGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_GGGA(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U5_GGGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), space, []), S1, P, T)
TURING_IN_GGGA(t(.(X, L), Y, R), S, P, T) → U7_GGGA(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GGGA(t(.(X, L), Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U7_GGGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_GGGA(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U7_GGGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t(L, X, .(W, R)), S1, P, T)
TURING_IN_GGGA(t([], Y, R), S, P, T) → U9_GGGA(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GGGA(t([], Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U9_GGGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_GGGA(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U9_GGGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t([], space, .(W, R)), S1, P, T)

The TRS R consists of the following rules:

turing_in_ggga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_ggga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U2_ggga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_ggga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_ggga(t(X, Y, .(R, L)), S, P, T) → U3_ggga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_ggga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_ggga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_gaga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
U2_gaga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_gaga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_gaga(t(X, Y, .(R, L)), S, P, T) → U3_gaga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_gaga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_gaga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, []), S, P, T) → U5_gaga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_gaga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_gaga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
turing_in_gaga(t(.(X, L), Y, R), S, P, T) → U7_gaga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_gaga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_gaga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
turing_in_gaga(t([], Y, R), S, P, T) → U9_gaga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_gaga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_gaga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_gaga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_gaga(t([], Y, R), S, P, T)
U8_gaga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_gaga(t(.(X, L), Y, R), S, P, T)
U6_gaga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_gaga(t(X, Y, []), S, P, T)
U4_gaga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_gaga(t(X, Y, .(R, L)), S, P, T)
U4_ggga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_ggga(t(X, Y, .(R, L)), S, P, T)
turing_in_ggga(t(X, Y, []), S, P, T) → U5_ggga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_ggga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_ggga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U6_ggga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_ggga(t(X, Y, []), S, P, T)
turing_in_ggga(t(.(X, L), Y, R), S, P, T) → U7_ggga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_ggga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_ggga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U8_ggga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_ggga(t(.(X, L), Y, R), S, P, T)
turing_in_ggga(t([], Y, R), S, P, T) → U9_ggga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_ggga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_ggga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_ggga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_ggga(t([], Y, R), S, P, T)

The argument filtering Pi contains the following mapping:
turing_in_ggga(x1, x2, x3, x4) = turing_in_ggga(x1, x2, x3)
t(x1, x2, x3) = t(x1, x3)
U2_ggga(x1, x2, x3, x4, x5, x6) = U2_ggga(x1, x3, x6)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
p(x1, x2, x3, x4, x5) = p
.(x1, x2) = .(x2)
member_out_gg(x1, x2) = member_out_gg
U1_gg(x1, x2, x3, x4) = U1_gg(x4)
halt = halt
turing_out_ggga(x1, x2, x3, x4) = turing_out_ggga(x4)
U3_ggga(x1, x2, x3, x4, x5, x6, x7, x8) = U3_ggga(x1, x4, x6, x8)
U4_ggga(x1, x2, x3, x4, x5, x6, x7, x8) = U4_ggga(x8)
turing_in_gaga(x1, x2, x3, x4) = turing_in_gaga(x1, x3)
U2_gaga(x1, x2, x3, x4, x5, x6) = U2_gaga(x1, x3, x6)
turing_out_gaga(x1, x2, x3, x4) = turing_out_gaga(x4)
U3_gaga(x1, x2, x3, x4, x5, x6, x7, x8) = U3_gaga(x1, x4, x6, x8)
U4_gaga(x1, x2, x3, x4, x5, x6, x7, x8) = U4_gaga(x8)
[] = []
U5_gaga(x1, x2, x3, x4, x5, x6) = U5_gaga(x1, x4, x6)
U6_gaga(x1, x2, x3, x4, x5, x6) = U6_gaga(x6)
U7_gaga(x1, x2, x3, x4, x5, x6, x7, x8) = U7_gaga(x2, x4, x6, x8)
U8_gaga(x1, x2, x3, x4, x5, x6, x7, x8) = U8_gaga(x8)
U9_gaga(x1, x2, x3, x4, x5, x6) = U9_gaga(x2, x4, x6)
U10_gaga(x1, x2, x3, x4, x5, x6) = U10_gaga(x6)
U5_ggga(x1, x2, x3, x4, x5, x6) = U5_ggga(x1, x4, x6)
U6_ggga(x1, x2, x3, x4, x5, x6) = U6_ggga(x6)
U7_ggga(x1, x2, x3, x4, x5, x6, x7, x8) = U7_ggga(x2, x4, x6, x8)
U8_ggga(x1, x2, x3, x4, x5, x6, x7, x8) = U8_ggga(x8)
U9_ggga(x1, x2, x3, x4, x5, x6) = U9_ggga(x2, x4, x6)
U10_ggga(x1, x2, x3, x4, x5, x6) = U10_ggga(x6)
TURING_IN_GGGA(x1, x2, x3, x4) = TURING_IN_GGGA(x1, x2, x3)
U6_GAGA(x1, x2, x3, x4, x5, x6) = U6_GAGA(x6)
TURING_IN_GAGA(x1, x2, x3, x4) = TURING_IN_GAGA(x1, x3)
U6_GGGA(x1, x2, x3, x4, x5, x6) = U6_GGGA(x6)
MEMBER_IN_GG(x1, x2) = MEMBER_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4) = U1_GG(x4)
U5_GAGA(x1, x2, x3, x4, x5, x6) = U5_GAGA(x1, x4, x6)
U7_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U7_GAGA(x2, x4, x6, x8)
U7_GGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U7_GGGA(x2, x4, x6, x8)
U2_GAGA(x1, x2, x3, x4, x5, x6) = U2_GAGA(x1, x3, x6)
U5_GGGA(x1, x2, x3, x4, x5, x6) = U5_GGGA(x1, x4, x6)
U4_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U4_GAGA(x8)
U3_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U3_GAGA(x1, x4, x6, x8)
U10_GAGA(x1, x2, x3, x4, x5, x6) = U10_GAGA(x6)
U3_GGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U3_GGGA(x1, x4, x6, x8)
U8_GGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U8_GGGA(x8)
U10_GGGA(x1, x2, x3, x4, x5, x6) = U10_GGGA(x6)
U9_GGGA(x1, x2, x3, x4, x5, x6) = U9_GGGA(x2, x4, x6)
U8_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U8_GAGA(x8)
U9_GAGA(x1, x2, x3, x4, x5, x6) = U9_GAGA(x2, x4, x6)
U4_GGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U4_GGGA(x8)
U2_GGGA(x1, x2, x3, x4, x5, x6) = U2_GGGA(x1, x3, x6)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

TURING_IN_GGGA(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_GGGA(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
TURING_IN_GGGA(t(X, Y, Z), S, P, t(X, Y, Z)) → MEMBER_IN_GG(p(S, Y, halt, W, D), P)
MEMBER_IN_GG(X, .(H, L)) → U1_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
TURING_IN_GGGA(t(X, Y, .(R, L)), S, P, T) → U3_GGGA(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GGGA(t(X, Y, .(R, L)), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U3_GGGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_GGGA(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
U3_GGGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), R, L), S1, P, T)
TURING_IN_GAGA(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_GAGA(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
TURING_IN_GAGA(t(X, Y, Z), S, P, t(X, Y, Z)) → MEMBER_IN_GG(p(S, Y, halt, W, D), P)
TURING_IN_GAGA(t(X, Y, .(R, L)), S, P, T) → U3_GAGA(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GAGA(t(X, Y, .(R, L)), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U3_GAGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_GAGA(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
U3_GAGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), R, L), S1, P, T)
TURING_IN_GAGA(t(X, Y, []), S, P, T) → U5_GAGA(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GAGA(t(X, Y, []), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U5_GAGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_GAGA(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U5_GAGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), space, []), S1, P, T)
TURING_IN_GAGA(t(.(X, L), Y, R), S, P, T) → U7_GAGA(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GAGA(t(.(X, L), Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U7_GAGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_GAGA(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U7_GAGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t(L, X, .(W, R)), S1, P, T)
TURING_IN_GAGA(t([], Y, R), S, P, T) → U9_GAGA(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GAGA(t([], Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U9_GAGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_GAGA(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U9_GAGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t([], space, .(W, R)), S1, P, T)
TURING_IN_GGGA(t(X, Y, []), S, P, T) → U5_GGGA(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GGGA(t(X, Y, []), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U5_GGGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_GGGA(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U5_GGGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), space, []), S1, P, T)
TURING_IN_GGGA(t(.(X, L), Y, R), S, P, T) → U7_GGGA(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GGGA(t(.(X, L), Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U7_GGGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_GGGA(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U7_GGGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t(L, X, .(W, R)), S1, P, T)
TURING_IN_GGGA(t([], Y, R), S, P, T) → U9_GGGA(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GGGA(t([], Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U9_GGGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_GGGA(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U9_GGGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t([], space, .(W, R)), S1, P, T)

The TRS R consists of the following rules:

turing_in_ggga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_ggga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U2_ggga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_ggga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_ggga(t(X, Y, .(R, L)), S, P, T) → U3_ggga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_ggga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_ggga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_gaga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
U2_gaga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_gaga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_gaga(t(X, Y, .(R, L)), S, P, T) → U3_gaga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_gaga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_gaga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, []), S, P, T) → U5_gaga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_gaga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_gaga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
turing_in_gaga(t(.(X, L), Y, R), S, P, T) → U7_gaga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_gaga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_gaga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
turing_in_gaga(t([], Y, R), S, P, T) → U9_gaga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_gaga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_gaga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_gaga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_gaga(t([], Y, R), S, P, T)
U8_gaga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_gaga(t(.(X, L), Y, R), S, P, T)
U6_gaga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_gaga(t(X, Y, []), S, P, T)
U4_gaga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_gaga(t(X, Y, .(R, L)), S, P, T)
U4_ggga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_ggga(t(X, Y, .(R, L)), S, P, T)
turing_in_ggga(t(X, Y, []), S, P, T) → U5_ggga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_ggga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_ggga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U6_ggga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_ggga(t(X, Y, []), S, P, T)
turing_in_ggga(t(.(X, L), Y, R), S, P, T) → U7_ggga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_ggga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_ggga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U8_ggga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_ggga(t(.(X, L), Y, R), S, P, T)
turing_in_ggga(t([], Y, R), S, P, T) → U9_ggga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_ggga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_ggga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_ggga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_ggga(t([], Y, R), S, P, T)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

The TRS R consists of the following rules:

turing_in_ggga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_ggga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U2_ggga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_ggga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_ggga(t(X, Y, .(R, L)), S, P, T) → U3_ggga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_ggga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_ggga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_gaga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
U2_gaga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_gaga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_gaga(t(X, Y, .(R, L)), S, P, T) → U3_gaga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_gaga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_gaga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, []), S, P, T) → U5_gaga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_gaga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_gaga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
turing_in_gaga(t(.(X, L), Y, R), S, P, T) → U7_gaga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_gaga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_gaga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
turing_in_gaga(t([], Y, R), S, P, T) → U9_gaga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_gaga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_gaga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_gaga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_gaga(t([], Y, R), S, P, T)
U8_gaga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_gaga(t(.(X, L), Y, R), S, P, T)
U6_gaga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_gaga(t(X, Y, []), S, P, T)
U4_gaga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_gaga(t(X, Y, .(R, L)), S, P, T)
U4_ggga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_ggga(t(X, Y, .(R, L)), S, P, T)
turing_in_ggga(t(X, Y, []), S, P, T) → U5_ggga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_ggga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_ggga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U6_ggga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_ggga(t(X, Y, []), S, P, T)
turing_in_ggga(t(.(X, L), Y, R), S, P, T) → U7_ggga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_ggga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_ggga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U8_ggga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_ggga(t(.(X, L), Y, R), S, P, T)
turing_in_ggga(t([], Y, R), S, P, T) → U9_ggga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_ggga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_ggga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_ggga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_ggga(t([], Y, R), S, P, T)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x2)
MEMBER_IN_GG(x1, x2) = MEMBER_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(L)) → MEMBER_IN_GG(X, L)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MEMBER_IN_GG(X, .(L)) → MEMBER_IN_GG(X, L)
The graph contains the following edges 1 >= 1, 2 > 2

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U3_GAGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), R, L), S1, P, T)
TURING_IN_GAGA(t(X, Y, .(R, L)), S, P, T) → U3_GAGA(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_GAGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), space, []), S1, P, T)
TURING_IN_GAGA(t([], Y, R), S, P, T) → U9_GAGA(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_GAGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t(L, X, .(W, R)), S1, P, T)
TURING_IN_GAGA(t(X, Y, []), S, P, T) → U5_GAGA(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U9_GAGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t([], space, .(W, R)), S1, P, T)
TURING_IN_GAGA(t(.(X, L), Y, R), S, P, T) → U7_GAGA(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))

The TRS R consists of the following rules:

turing_in_ggga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_ggga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U2_ggga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_ggga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_ggga(t(X, Y, .(R, L)), S, P, T) → U3_ggga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_ggga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_ggga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_gaga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
U2_gaga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_gaga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_gaga(t(X, Y, .(R, L)), S, P, T) → U3_gaga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_gaga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_gaga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, []), S, P, T) → U5_gaga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_gaga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_gaga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
turing_in_gaga(t(.(X, L), Y, R), S, P, T) → U7_gaga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_gaga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_gaga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
turing_in_gaga(t([], Y, R), S, P, T) → U9_gaga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_gaga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_gaga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_gaga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_gaga(t([], Y, R), S, P, T)
U8_gaga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_gaga(t(.(X, L), Y, R), S, P, T)
U6_gaga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_gaga(t(X, Y, []), S, P, T)
U4_gaga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_gaga(t(X, Y, .(R, L)), S, P, T)
U4_ggga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_ggga(t(X, Y, .(R, L)), S, P, T)
turing_in_ggga(t(X, Y, []), S, P, T) → U5_ggga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_ggga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_ggga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U6_ggga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_ggga(t(X, Y, []), S, P, T)
turing_in_ggga(t(.(X, L), Y, R), S, P, T) → U7_ggga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_ggga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_ggga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U8_ggga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_ggga(t(.(X, L), Y, R), S, P, T)
turing_in_ggga(t([], Y, R), S, P, T) → U9_ggga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_ggga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_ggga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_ggga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_ggga(t([], Y, R), S, P, T)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U3_GAGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), R, L), S1, P, T)
TURING_IN_GAGA(t(X, Y, .(R, L)), S, P, T) → U3_GAGA(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_GAGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), space, []), S1, P, T)
TURING_IN_GAGA(t([], Y, R), S, P, T) → U9_GAGA(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_GAGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t(L, X, .(W, R)), S1, P, T)
TURING_IN_GAGA(t(X, Y, []), S, P, T) → U5_GAGA(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U9_GAGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t([], space, .(W, R)), S1, P, T)
TURING_IN_GAGA(t(.(X, L), Y, R), S, P, T) → U7_GAGA(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))

The TRS R consists of the following rules:

member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))

The argument filtering Pi contains the following mapping:
t(x1, x2, x3) = t(x1, x3)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
p(x1, x2, x3, x4, x5) = p
.(x1, x2) = .(x2)
member_out_gg(x1, x2) = member_out_gg
U1_gg(x1, x2, x3, x4) = U1_gg(x4)
[] = []
TURING_IN_GAGA(x1, x2, x3, x4) = TURING_IN_GAGA(x1, x3)
U5_GAGA(x1, x2, x3, x4, x5, x6) = U5_GAGA(x1, x4, x6)
U7_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U7_GAGA(x2, x4, x6, x8)
U3_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U3_GAGA(x1, x4, x6, x8)
U9_GAGA(x1, x2, x3, x4, x5, x6) = U9_GAGA(x2, x4, x6)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

TURING_IN_GAGA(t(X, []), P) → U5_GAGA(X, P, member_in_gg(p, P))
U9_GAGA(R, P, member_out_gg) → TURING_IN_GAGA(t([], .(R)), P)
U7_GAGA(L, R, P, member_out_gg) → TURING_IN_GAGA(t(L, .(R)), P)
TURING_IN_GAGA(t([], R), P) → U9_GAGA(R, P, member_in_gg(p, P))
TURING_IN_GAGA(t(.(L), R), P) → U7_GAGA(L, R, P, member_in_gg(p, P))
U3_GAGA(X, L, P, member_out_gg) → TURING_IN_GAGA(t(.(X), L), P)
TURING_IN_GAGA(t(X, .(L)), P) → U3_GAGA(X, L, P, member_in_gg(p, P))
U5_GAGA(X, P, member_out_gg) → TURING_IN_GAGA(t(.(X), []), P)

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule TURING_IN_GAGA(t(X, .(L)), P) → U3_GAGA(X, L, P, member_in_gg(p, P)) at position [3] we obtained the following new rules:

TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

TURING_IN_GAGA(t(X, []), P) → U5_GAGA(X, P, member_in_gg(p, P))
U7_GAGA(L, R, P, member_out_gg) → TURING_IN_GAGA(t(L, .(R)), P)
U9_GAGA(R, P, member_out_gg) → TURING_IN_GAGA(t([], .(R)), P)
TURING_IN_GAGA(t([], R), P) → U9_GAGA(R, P, member_in_gg(p, P))
U3_GAGA(X, L, P, member_out_gg) → TURING_IN_GAGA(t(.(X), L), P)
TURING_IN_GAGA(t(.(L), R), P) → U7_GAGA(L, R, P, member_in_gg(p, P))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
U5_GAGA(X, P, member_out_gg) → TURING_IN_GAGA(t(.(X), []), P)

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule TURING_IN_GAGA(t([], R), P) → U9_GAGA(R, P, member_in_gg(p, P)) at position [2] we obtained the following new rules:

TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

TURING_IN_GAGA(t(X, []), P) → U5_GAGA(X, P, member_in_gg(p, P))
U9_GAGA(R, P, member_out_gg) → TURING_IN_GAGA(t([], .(R)), P)
U7_GAGA(L, R, P, member_out_gg) → TURING_IN_GAGA(t(L, .(R)), P)
TURING_IN_GAGA(t(.(L), R), P) → U7_GAGA(L, R, P, member_in_gg(p, P))
U3_GAGA(X, L, P, member_out_gg) → TURING_IN_GAGA(t(.(X), L), P)
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))
U5_GAGA(X, P, member_out_gg) → TURING_IN_GAGA(t(.(X), []), P)

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule TURING_IN_GAGA(t(X, []), P) → U5_GAGA(X, P, member_in_gg(p, P)) at position [2] we obtained the following new rules:

TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U7_GAGA(L, R, P, member_out_gg) → TURING_IN_GAGA(t(L, .(R)), P)
U9_GAGA(R, P, member_out_gg) → TURING_IN_GAGA(t([], .(R)), P)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))
U3_GAGA(X, L, P, member_out_gg) → TURING_IN_GAGA(t(.(X), L), P)
TURING_IN_GAGA(t(.(L), R), P) → U7_GAGA(L, R, P, member_in_gg(p, P))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))
U5_GAGA(X, P, member_out_gg) → TURING_IN_GAGA(t(.(X), []), P)

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule TURING_IN_GAGA(t(.(L), R), P) → U7_GAGA(L, R, P, member_in_gg(p, P)) at position [3] we obtained the following new rules:

TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg)
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U7_GAGA(L, R, P, member_out_gg) → TURING_IN_GAGA(t(L, .(R)), P)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))
U3_GAGA(X, L, P, member_out_gg) → TURING_IN_GAGA(t(.(X), L), P)
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg)
U9_GAGA(R, P, member_out_gg) → TURING_IN_GAGA(t([], .(R)), P)
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))
U5_GAGA(X, P, member_out_gg) → TURING_IN_GAGA(t(.(X), []), P)

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U3_GAGA(X, L, P, member_out_gg) → TURING_IN_GAGA(t(.(X), L), P) we obtained the following new rules:

U3_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(.(z0), z1), .(z2))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U3_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
U7_GAGA(L, R, P, member_out_gg) → TURING_IN_GAGA(t(L, .(R)), P)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg)
U9_GAGA(R, P, member_out_gg) → TURING_IN_GAGA(t([], .(R)), P)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))
U5_GAGA(X, P, member_out_gg) → TURING_IN_GAGA(t(.(X), []), P)

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U5_GAGA(X, P, member_out_gg) → TURING_IN_GAGA(t(.(X), []), P) we obtained the following new rules:

U5_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t(.(z0), []), .(z1))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t(.(z0), []), .(z1))
U7_GAGA(L, R, P, member_out_gg) → TURING_IN_GAGA(t(L, .(R)), P)
U3_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg)
U9_GAGA(R, P, member_out_gg) → TURING_IN_GAGA(t([], .(R)), P)
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U7_GAGA(L, R, P, member_out_gg) → TURING_IN_GAGA(t(L, .(R)), P) we obtained the following new rules:

U7_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t(.(z0), []), .(z1))
U3_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg)
U9_GAGA(R, P, member_out_gg) → TURING_IN_GAGA(t([], .(R)), P)
U7_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U9_GAGA(R, P, member_out_gg) → TURING_IN_GAGA(t([], .(R)), P) we obtained the following new rules:

U9_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t([], .(z0)), .(z1))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t(.(z0), []), .(z1))
U3_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg)
U7_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg)
U9_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t([], .(z0)), .(z1))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg) we obtained the following new rules:

TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

                                                          ↳ QDP

                                                            ↳ Instantiation

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t(.(z0), []), .(z1))
U3_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg)
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg)
U7_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg)
U9_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t([], .(z0)), .(z1))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1))) we obtained the following new rules:

TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(member_in_gg(p, z2)))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

                                                          ↳ QDP

                                                            ↳ Instantiation

                                                              ↳ QDP

                                                                ↳ Instantiation

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t(.(z0), []), .(z1))
U3_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg)
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg)
U7_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(member_in_gg(p, z2)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg)
U9_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t([], .(z0)), .(z1))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg) we obtained the following new rules:

TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), member_out_gg)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

                                                          ↳ QDP

                                                            ↳ Instantiation

                                                              ↳ QDP

                                                                ↳ Instantiation

                                                                  ↳ QDP

                                                                    ↳ Instantiation

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t(.(z0), []), .(z1))
U3_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), member_out_gg)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg)
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg)
U7_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(member_in_gg(p, z2)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
U9_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t([], .(z0)), .(z1))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(member_in_gg(p, x1))) we obtained the following new rules:

TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), U1_gg(member_in_gg(p, z2)))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

                                                          ↳ QDP

                                                            ↳ Instantiation

                                                              ↳ QDP

                                                                ↳ Instantiation

                                                                  ↳ QDP

                                                                    ↳ Instantiation

                                                                      ↳ QDP

                                                                        ↳ Instantiation

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t(.(z0), []), .(z1))
U3_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), member_out_gg)
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg)
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), U1_gg(member_in_gg(p, z2)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg)
U7_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(member_in_gg(p, z2)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
U9_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t([], .(z0)), .(z1))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U5_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t(.(z0), []), .(z1)) we obtained the following new rules:

U5_GAGA(.(z0), .(z1), member_out_gg) → TURING_IN_GAGA(t(.(.(z0)), []), .(z1))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

                                                          ↳ QDP

                                                            ↳ Instantiation

                                                              ↳ QDP

                                                                ↳ Instantiation

                                                                  ↳ QDP

                                                                    ↳ Instantiation

                                                                      ↳ QDP

                                                                        ↳ Instantiation

                                                                          ↳ QDP

                                                                            ↳ Instantiation

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U3_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), member_out_gg)
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg)
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg)
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), U1_gg(member_in_gg(p, z2)))
U5_GAGA(.(z0), .(z1), member_out_gg) → TURING_IN_GAGA(t(.(.(z0)), []), .(z1))
U7_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(member_in_gg(p, z2)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)
U9_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t([], .(z0)), .(z1))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U9_GAGA(z0, .(z1), member_out_gg) → TURING_IN_GAGA(t([], .(z0)), .(z1)) we obtained the following new rules:

U9_GAGA(.(z0), .(z1), member_out_gg) → TURING_IN_GAGA(t([], .(.(z0))), .(z1))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

                                                          ↳ QDP

                                                            ↳ Instantiation

                                                              ↳ QDP

                                                                ↳ Instantiation

                                                                  ↳ QDP

                                                                    ↳ Instantiation

                                                                      ↳ QDP

                                                                        ↳ Instantiation

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ NonTerminationProof

  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U3_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), member_out_gg)
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg)
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), U1_gg(member_in_gg(p, z2)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg)
U5_GAGA(.(z0), .(z1), member_out_gg) → TURING_IN_GAGA(t(.(.(z0)), []), .(z1))
U7_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))
U9_GAGA(.(z0), .(z1), member_out_gg) → TURING_IN_GAGA(t([], .(.(z0))), .(z1))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(member_in_gg(p, z2)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0)

We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

U3_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), member_out_gg)
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(member_in_gg(p, x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg)
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), U1_gg(member_in_gg(p, z2)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg)
U5_GAGA(.(z0), .(z1), member_out_gg) → TURING_IN_GAGA(t(.(.(z0)), []), .(z1))
U7_GAGA(z0, z1, .(z2), member_out_gg) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))
U9_GAGA(.(z0), .(z1), member_out_gg) → TURING_IN_GAGA(t([], .(.(z0))), .(z1))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(member_in_gg(p, z2)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg)

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg
member_in_gg(X, .(L)) → U1_gg(member_in_gg(X, L))
U1_gg(member_out_gg) → member_out_gg

s = U5_GAGA(.(z0'), .(z1), member_out_gg) evaluates to t =U5_GAGA(.(.(z0')), .(z1), member_out_gg)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [z0' / .(z0')]
Semiunifier: [ ]

Rewriting sequence

U5_GAGA(.(z0'), .(z1), member_out_gg) → TURING_IN_GAGA(t(.(.(z0')), []), .(z1))
with rule U5_GAGA(.(z0''), .(z1'), member_out_gg) → TURING_IN_GAGA(t(.(.(z0'')), []), .(z1')) at position [] and matcher [z1' / z1, z0'' / z0']

TURING_IN_GAGA(t(.(.(z0')), []), .(z1)) → U5_GAGA(.(.(z0')), .(z1), member_out_gg)
with rule TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), member_out_gg)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
turing_in: (b,b,b,f) (b,f,b,f)
member_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

turing_in_ggga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_ggga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U2_ggga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_ggga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_ggga(t(X, Y, .(R, L)), S, P, T) → U3_ggga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_ggga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_ggga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_gaga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
U2_gaga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_gaga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_gaga(t(X, Y, .(R, L)), S, P, T) → U3_gaga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_gaga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_gaga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, []), S, P, T) → U5_gaga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_gaga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_gaga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
turing_in_gaga(t(.(X, L), Y, R), S, P, T) → U7_gaga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_gaga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_gaga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
turing_in_gaga(t([], Y, R), S, P, T) → U9_gaga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_gaga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_gaga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_gaga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_gaga(t([], Y, R), S, P, T)
U8_gaga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_gaga(t(.(X, L), Y, R), S, P, T)
U6_gaga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_gaga(t(X, Y, []), S, P, T)
U4_gaga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_gaga(t(X, Y, .(R, L)), S, P, T)
U4_ggga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_ggga(t(X, Y, .(R, L)), S, P, T)
turing_in_ggga(t(X, Y, []), S, P, T) → U5_ggga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_ggga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_ggga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U6_ggga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_ggga(t(X, Y, []), S, P, T)
turing_in_ggga(t(.(X, L), Y, R), S, P, T) → U7_ggga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_ggga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_ggga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U8_ggga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_ggga(t(.(X, L), Y, R), S, P, T)
turing_in_ggga(t([], Y, R), S, P, T) → U9_ggga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_ggga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_ggga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_ggga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_ggga(t([], Y, R), S, P, T)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

turing_in_ggga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_ggga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U2_ggga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_ggga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_ggga(t(X, Y, .(R, L)), S, P, T) → U3_ggga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_ggga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_ggga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_gaga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
U2_gaga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_gaga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_gaga(t(X, Y, .(R, L)), S, P, T) → U3_gaga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_gaga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_gaga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, []), S, P, T) → U5_gaga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_gaga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_gaga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
turing_in_gaga(t(.(X, L), Y, R), S, P, T) → U7_gaga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_gaga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_gaga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
turing_in_gaga(t([], Y, R), S, P, T) → U9_gaga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_gaga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_gaga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_gaga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_gaga(t([], Y, R), S, P, T)
U8_gaga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_gaga(t(.(X, L), Y, R), S, P, T)
U6_gaga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_gaga(t(X, Y, []), S, P, T)
U4_gaga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_gaga(t(X, Y, .(R, L)), S, P, T)
U4_ggga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_ggga(t(X, Y, .(R, L)), S, P, T)
turing_in_ggga(t(X, Y, []), S, P, T) → U5_ggga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_ggga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_ggga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U6_ggga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_ggga(t(X, Y, []), S, P, T)
turing_in_ggga(t(.(X, L), Y, R), S, P, T) → U7_ggga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_ggga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_ggga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U8_ggga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_ggga(t(.(X, L), Y, R), S, P, T)
turing_in_ggga(t([], Y, R), S, P, T) → U9_ggga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_ggga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_ggga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_ggga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_ggga(t([], Y, R), S, P, T)

TURING_IN_GGGA(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_GGGA(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
TURING_IN_GGGA(t(X, Y, Z), S, P, t(X, Y, Z)) → MEMBER_IN_GG(p(S, Y, halt, W, D), P)
MEMBER_IN_GG(X, .(H, L)) → U1_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
TURING_IN_GGGA(t(X, Y, .(R, L)), S, P, T) → U3_GGGA(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GGGA(t(X, Y, .(R, L)), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U3_GGGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_GGGA(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
U3_GGGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), R, L), S1, P, T)
TURING_IN_GAGA(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_GAGA(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
TURING_IN_GAGA(t(X, Y, Z), S, P, t(X, Y, Z)) → MEMBER_IN_GG(p(S, Y, halt, W, D), P)
TURING_IN_GAGA(t(X, Y, .(R, L)), S, P, T) → U3_GAGA(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GAGA(t(X, Y, .(R, L)), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U3_GAGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_GAGA(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
U3_GAGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), R, L), S1, P, T)
TURING_IN_GAGA(t(X, Y, []), S, P, T) → U5_GAGA(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GAGA(t(X, Y, []), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U5_GAGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_GAGA(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U5_GAGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), space, []), S1, P, T)
TURING_IN_GAGA(t(.(X, L), Y, R), S, P, T) → U7_GAGA(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GAGA(t(.(X, L), Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U7_GAGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_GAGA(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U7_GAGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t(L, X, .(W, R)), S1, P, T)
TURING_IN_GAGA(t([], Y, R), S, P, T) → U9_GAGA(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GAGA(t([], Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U9_GAGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_GAGA(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U9_GAGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t([], space, .(W, R)), S1, P, T)
TURING_IN_GGGA(t(X, Y, []), S, P, T) → U5_GGGA(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GGGA(t(X, Y, []), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U5_GGGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_GGGA(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U5_GGGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), space, []), S1, P, T)
TURING_IN_GGGA(t(.(X, L), Y, R), S, P, T) → U7_GGGA(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GGGA(t(.(X, L), Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U7_GGGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_GGGA(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U7_GGGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t(L, X, .(W, R)), S1, P, T)
TURING_IN_GGGA(t([], Y, R), S, P, T) → U9_GGGA(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GGGA(t([], Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U9_GGGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_GGGA(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U9_GGGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t([], space, .(W, R)), S1, P, T)

The TRS R consists of the following rules:

turing_in_ggga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_ggga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U2_ggga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_ggga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_ggga(t(X, Y, .(R, L)), S, P, T) → U3_ggga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_ggga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_ggga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_gaga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
U2_gaga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_gaga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_gaga(t(X, Y, .(R, L)), S, P, T) → U3_gaga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_gaga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_gaga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, []), S, P, T) → U5_gaga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_gaga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_gaga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
turing_in_gaga(t(.(X, L), Y, R), S, P, T) → U7_gaga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_gaga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_gaga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
turing_in_gaga(t([], Y, R), S, P, T) → U9_gaga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_gaga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_gaga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_gaga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_gaga(t([], Y, R), S, P, T)
U8_gaga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_gaga(t(.(X, L), Y, R), S, P, T)
U6_gaga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_gaga(t(X, Y, []), S, P, T)
U4_gaga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_gaga(t(X, Y, .(R, L)), S, P, T)
U4_ggga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_ggga(t(X, Y, .(R, L)), S, P, T)
turing_in_ggga(t(X, Y, []), S, P, T) → U5_ggga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_ggga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_ggga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U6_ggga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_ggga(t(X, Y, []), S, P, T)
turing_in_ggga(t(.(X, L), Y, R), S, P, T) → U7_ggga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_ggga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_ggga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U8_ggga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_ggga(t(.(X, L), Y, R), S, P, T)
turing_in_ggga(t([], Y, R), S, P, T) → U9_ggga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_ggga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_ggga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_ggga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_ggga(t([], Y, R), S, P, T)

The argument filtering Pi contains the following mapping:
turing_in_ggga(x1, x2, x3, x4) = turing_in_ggga(x1, x2, x3)
t(x1, x2, x3) = t(x1, x3)
U2_ggga(x1, x2, x3, x4, x5, x6) = U2_ggga(x1, x3, x4, x5, x6)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
p(x1, x2, x3, x4, x5) = p
.(x1, x2) = .(x2)
member_out_gg(x1, x2) = member_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4) = U1_gg(x1, x3, x4)
halt = halt
turing_out_ggga(x1, x2, x3, x4) = turing_out_ggga(x1, x2, x3, x4)
U3_ggga(x1, x2, x3, x4, x5, x6, x7, x8) = U3_ggga(x1, x4, x5, x6, x8)
U4_ggga(x1, x2, x3, x4, x5, x6, x7, x8) = U4_ggga(x1, x4, x5, x6, x8)
turing_in_gaga(x1, x2, x3, x4) = turing_in_gaga(x1, x3)
U2_gaga(x1, x2, x3, x4, x5, x6) = U2_gaga(x1, x3, x5, x6)
turing_out_gaga(x1, x2, x3, x4) = turing_out_gaga(x1, x3, x4)
U3_gaga(x1, x2, x3, x4, x5, x6, x7, x8) = U3_gaga(x1, x4, x6, x8)
U4_gaga(x1, x2, x3, x4, x5, x6, x7, x8) = U4_gaga(x1, x4, x6, x8)
[] = []
U5_gaga(x1, x2, x3, x4, x5, x6) = U5_gaga(x1, x4, x6)
U6_gaga(x1, x2, x3, x4, x5, x6) = U6_gaga(x1, x4, x6)
U7_gaga(x1, x2, x3, x4, x5, x6, x7, x8) = U7_gaga(x2, x4, x6, x8)
U8_gaga(x1, x2, x3, x4, x5, x6, x7, x8) = U8_gaga(x2, x4, x6, x8)
U9_gaga(x1, x2, x3, x4, x5, x6) = U9_gaga(x2, x4, x6)
U10_gaga(x1, x2, x3, x4, x5, x6) = U10_gaga(x2, x4, x6)
U5_ggga(x1, x2, x3, x4, x5, x6) = U5_ggga(x1, x3, x4, x6)
U6_ggga(x1, x2, x3, x4, x5, x6) = U6_ggga(x1, x3, x4, x6)
U7_ggga(x1, x2, x3, x4, x5, x6, x7, x8) = U7_ggga(x2, x4, x5, x6, x8)
U8_ggga(x1, x2, x3, x4, x5, x6, x7, x8) = U8_ggga(x2, x4, x5, x6, x8)
U9_ggga(x1, x2, x3, x4, x5, x6) = U9_ggga(x2, x3, x4, x6)
U10_ggga(x1, x2, x3, x4, x5, x6) = U10_ggga(x2, x3, x4, x6)
TURING_IN_GGGA(x1, x2, x3, x4) = TURING_IN_GGGA(x1, x2, x3)
U6_GAGA(x1, x2, x3, x4, x5, x6) = U6_GAGA(x1, x4, x6)
TURING_IN_GAGA(x1, x2, x3, x4) = TURING_IN_GAGA(x1, x3)
U6_GGGA(x1, x2, x3, x4, x5, x6) = U6_GGGA(x1, x3, x4, x6)
MEMBER_IN_GG(x1, x2) = MEMBER_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4) = U1_GG(x1, x3, x4)
U5_GAGA(x1, x2, x3, x4, x5, x6) = U5_GAGA(x1, x4, x6)
U7_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U7_GAGA(x2, x4, x6, x8)
U7_GGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U7_GGGA(x2, x4, x5, x6, x8)
U2_GAGA(x1, x2, x3, x4, x5, x6) = U2_GAGA(x1, x3, x5, x6)
U5_GGGA(x1, x2, x3, x4, x5, x6) = U5_GGGA(x1, x3, x4, x6)
U4_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U4_GAGA(x1, x4, x6, x8)
U3_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U3_GAGA(x1, x4, x6, x8)
U10_GAGA(x1, x2, x3, x4, x5, x6) = U10_GAGA(x2, x4, x6)
U3_GGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U3_GGGA(x1, x4, x5, x6, x8)
U8_GGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U8_GGGA(x2, x4, x5, x6, x8)
U10_GGGA(x1, x2, x3, x4, x5, x6) = U10_GGGA(x2, x3, x4, x6)
U9_GGGA(x1, x2, x3, x4, x5, x6) = U9_GGGA(x2, x3, x4, x6)
U8_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U8_GAGA(x2, x4, x6, x8)
U9_GAGA(x1, x2, x3, x4, x5, x6) = U9_GAGA(x2, x4, x6)
U4_GGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U4_GGGA(x1, x4, x5, x6, x8)
U2_GGGA(x1, x2, x3, x4, x5, x6) = U2_GGGA(x1, x3, x4, x5, x6)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

TURING_IN_GGGA(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_GGGA(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
TURING_IN_GGGA(t(X, Y, Z), S, P, t(X, Y, Z)) → MEMBER_IN_GG(p(S, Y, halt, W, D), P)
MEMBER_IN_GG(X, .(H, L)) → U1_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
TURING_IN_GGGA(t(X, Y, .(R, L)), S, P, T) → U3_GGGA(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GGGA(t(X, Y, .(R, L)), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U3_GGGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_GGGA(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
U3_GGGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), R, L), S1, P, T)
TURING_IN_GAGA(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_GAGA(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
TURING_IN_GAGA(t(X, Y, Z), S, P, t(X, Y, Z)) → MEMBER_IN_GG(p(S, Y, halt, W, D), P)
TURING_IN_GAGA(t(X, Y, .(R, L)), S, P, T) → U3_GAGA(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GAGA(t(X, Y, .(R, L)), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U3_GAGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_GAGA(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
U3_GAGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), R, L), S1, P, T)
TURING_IN_GAGA(t(X, Y, []), S, P, T) → U5_GAGA(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GAGA(t(X, Y, []), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U5_GAGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_GAGA(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U5_GAGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), space, []), S1, P, T)
TURING_IN_GAGA(t(.(X, L), Y, R), S, P, T) → U7_GAGA(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GAGA(t(.(X, L), Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U7_GAGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_GAGA(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U7_GAGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t(L, X, .(W, R)), S1, P, T)
TURING_IN_GAGA(t([], Y, R), S, P, T) → U9_GAGA(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GAGA(t([], Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U9_GAGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_GAGA(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U9_GAGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t([], space, .(W, R)), S1, P, T)
TURING_IN_GGGA(t(X, Y, []), S, P, T) → U5_GGGA(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
TURING_IN_GGGA(t(X, Y, []), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, r), P)
U5_GGGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_GGGA(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U5_GGGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), space, []), S1, P, T)
TURING_IN_GGGA(t(.(X, L), Y, R), S, P, T) → U7_GGGA(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GGGA(t(.(X, L), Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U7_GGGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_GGGA(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U7_GGGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t(L, X, .(W, R)), S1, P, T)
TURING_IN_GGGA(t([], Y, R), S, P, T) → U9_GGGA(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
TURING_IN_GGGA(t([], Y, R), S, P, T) → MEMBER_IN_GG(p(S, Y, S1, W, l), P)
U9_GGGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_GGGA(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U9_GGGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t([], space, .(W, R)), S1, P, T)

The TRS R consists of the following rules:

turing_in_ggga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_ggga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U2_ggga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_ggga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_ggga(t(X, Y, .(R, L)), S, P, T) → U3_ggga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_ggga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_ggga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_gaga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
U2_gaga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_gaga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_gaga(t(X, Y, .(R, L)), S, P, T) → U3_gaga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_gaga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_gaga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, []), S, P, T) → U5_gaga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_gaga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_gaga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
turing_in_gaga(t(.(X, L), Y, R), S, P, T) → U7_gaga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_gaga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_gaga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
turing_in_gaga(t([], Y, R), S, P, T) → U9_gaga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_gaga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_gaga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_gaga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_gaga(t([], Y, R), S, P, T)
U8_gaga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_gaga(t(.(X, L), Y, R), S, P, T)
U6_gaga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_gaga(t(X, Y, []), S, P, T)
U4_gaga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_gaga(t(X, Y, .(R, L)), S, P, T)
U4_ggga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_ggga(t(X, Y, .(R, L)), S, P, T)
turing_in_ggga(t(X, Y, []), S, P, T) → U5_ggga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_ggga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_ggga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U6_ggga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_ggga(t(X, Y, []), S, P, T)
turing_in_ggga(t(.(X, L), Y, R), S, P, T) → U7_ggga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_ggga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_ggga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U8_ggga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_ggga(t(.(X, L), Y, R), S, P, T)
turing_in_ggga(t([], Y, R), S, P, T) → U9_ggga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_ggga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_ggga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_ggga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_ggga(t([], Y, R), S, P, T)

The argument filtering Pi contains the following mapping:
turing_in_ggga(x1, x2, x3, x4) = turing_in_ggga(x1, x2, x3)
t(x1, x2, x3) = t(x1, x3)
U2_ggga(x1, x2, x3, x4, x5, x6) = U2_ggga(x1, x3, x4, x5, x6)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
p(x1, x2, x3, x4, x5) = p
.(x1, x2) = .(x2)
member_out_gg(x1, x2) = member_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4) = U1_gg(x1, x3, x4)
halt = halt
turing_out_ggga(x1, x2, x3, x4) = turing_out_ggga(x1, x2, x3, x4)
U3_ggga(x1, x2, x3, x4, x5, x6, x7, x8) = U3_ggga(x1, x4, x5, x6, x8)
U4_ggga(x1, x2, x3, x4, x5, x6, x7, x8) = U4_ggga(x1, x4, x5, x6, x8)
turing_in_gaga(x1, x2, x3, x4) = turing_in_gaga(x1, x3)
U2_gaga(x1, x2, x3, x4, x5, x6) = U2_gaga(x1, x3, x5, x6)
turing_out_gaga(x1, x2, x3, x4) = turing_out_gaga(x1, x3, x4)
U3_gaga(x1, x2, x3, x4, x5, x6, x7, x8) = U3_gaga(x1, x4, x6, x8)
U4_gaga(x1, x2, x3, x4, x5, x6, x7, x8) = U4_gaga(x1, x4, x6, x8)
[] = []
U5_gaga(x1, x2, x3, x4, x5, x6) = U5_gaga(x1, x4, x6)
U6_gaga(x1, x2, x3, x4, x5, x6) = U6_gaga(x1, x4, x6)
U7_gaga(x1, x2, x3, x4, x5, x6, x7, x8) = U7_gaga(x2, x4, x6, x8)
U8_gaga(x1, x2, x3, x4, x5, x6, x7, x8) = U8_gaga(x2, x4, x6, x8)
U9_gaga(x1, x2, x3, x4, x5, x6) = U9_gaga(x2, x4, x6)
U10_gaga(x1, x2, x3, x4, x5, x6) = U10_gaga(x2, x4, x6)
U5_ggga(x1, x2, x3, x4, x5, x6) = U5_ggga(x1, x3, x4, x6)
U6_ggga(x1, x2, x3, x4, x5, x6) = U6_ggga(x1, x3, x4, x6)
U7_ggga(x1, x2, x3, x4, x5, x6, x7, x8) = U7_ggga(x2, x4, x5, x6, x8)
U8_ggga(x1, x2, x3, x4, x5, x6, x7, x8) = U8_ggga(x2, x4, x5, x6, x8)
U9_ggga(x1, x2, x3, x4, x5, x6) = U9_ggga(x2, x3, x4, x6)
U10_ggga(x1, x2, x3, x4, x5, x6) = U10_ggga(x2, x3, x4, x6)
TURING_IN_GGGA(x1, x2, x3, x4) = TURING_IN_GGGA(x1, x2, x3)
U6_GAGA(x1, x2, x3, x4, x5, x6) = U6_GAGA(x1, x4, x6)
TURING_IN_GAGA(x1, x2, x3, x4) = TURING_IN_GAGA(x1, x3)
U6_GGGA(x1, x2, x3, x4, x5, x6) = U6_GGGA(x1, x3, x4, x6)
MEMBER_IN_GG(x1, x2) = MEMBER_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4) = U1_GG(x1, x3, x4)
U5_GAGA(x1, x2, x3, x4, x5, x6) = U5_GAGA(x1, x4, x6)
U7_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U7_GAGA(x2, x4, x6, x8)
U7_GGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U7_GGGA(x2, x4, x5, x6, x8)
U2_GAGA(x1, x2, x3, x4, x5, x6) = U2_GAGA(x1, x3, x5, x6)
U5_GGGA(x1, x2, x3, x4, x5, x6) = U5_GGGA(x1, x3, x4, x6)
U4_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U4_GAGA(x1, x4, x6, x8)
U3_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U3_GAGA(x1, x4, x6, x8)
U10_GAGA(x1, x2, x3, x4, x5, x6) = U10_GAGA(x2, x4, x6)
U3_GGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U3_GGGA(x1, x4, x5, x6, x8)
U8_GGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U8_GGGA(x2, x4, x5, x6, x8)
U10_GGGA(x1, x2, x3, x4, x5, x6) = U10_GGGA(x2, x3, x4, x6)
U9_GGGA(x1, x2, x3, x4, x5, x6) = U9_GGGA(x2, x3, x4, x6)
U8_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U8_GAGA(x2, x4, x6, x8)
U9_GAGA(x1, x2, x3, x4, x5, x6) = U9_GAGA(x2, x4, x6)
U4_GGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U4_GGGA(x1, x4, x5, x6, x8)
U2_GGGA(x1, x2, x3, x4, x5, x6) = U2_GGGA(x1, x3, x4, x5, x6)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 2 SCCs with 29 less nodes.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

The TRS R consists of the following rules:

turing_in_ggga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_ggga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U2_ggga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_ggga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_ggga(t(X, Y, .(R, L)), S, P, T) → U3_ggga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_ggga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_ggga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_gaga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
U2_gaga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_gaga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_gaga(t(X, Y, .(R, L)), S, P, T) → U3_gaga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_gaga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_gaga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, []), S, P, T) → U5_gaga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_gaga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_gaga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
turing_in_gaga(t(.(X, L), Y, R), S, P, T) → U7_gaga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_gaga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_gaga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
turing_in_gaga(t([], Y, R), S, P, T) → U9_gaga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_gaga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_gaga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_gaga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_gaga(t([], Y, R), S, P, T)
U8_gaga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_gaga(t(.(X, L), Y, R), S, P, T)
U6_gaga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_gaga(t(X, Y, []), S, P, T)
U4_gaga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_gaga(t(X, Y, .(R, L)), S, P, T)
U4_ggga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_ggga(t(X, Y, .(R, L)), S, P, T)
turing_in_ggga(t(X, Y, []), S, P, T) → U5_ggga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_ggga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_ggga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U6_ggga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_ggga(t(X, Y, []), S, P, T)
turing_in_ggga(t(.(X, L), Y, R), S, P, T) → U7_ggga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_ggga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_ggga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U8_ggga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_ggga(t(.(X, L), Y, R), S, P, T)
turing_in_ggga(t([], Y, R), S, P, T) → U9_ggga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_ggga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_ggga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_ggga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_ggga(t([], Y, R), S, P, T)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(L)) → MEMBER_IN_GG(X, L)

From the DPs we obtained the following set of size-change graphs:

MEMBER_IN_GG(X, .(L)) → MEMBER_IN_GG(X, L)
The graph contains the following edges 1 >= 1, 2 > 2

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

U3_GAGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), R, L), S1, P, T)
TURING_IN_GAGA(t(X, Y, .(R, L)), S, P, T) → U3_GAGA(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_GAGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), space, []), S1, P, T)
TURING_IN_GAGA(t([], Y, R), S, P, T) → U9_GAGA(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_GAGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t(L, X, .(W, R)), S1, P, T)
TURING_IN_GAGA(t(X, Y, []), S, P, T) → U5_GAGA(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U9_GAGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t([], space, .(W, R)), S1, P, T)
TURING_IN_GAGA(t(.(X, L), Y, R), S, P, T) → U7_GAGA(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))

The TRS R consists of the following rules:

turing_in_ggga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_ggga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U2_ggga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_ggga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_ggga(t(X, Y, .(R, L)), S, P, T) → U3_ggga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_ggga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_ggga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, Z), S, P, t(X, Y, Z)) → U2_gaga(X, Y, Z, S, P, member_in_gg(p(S, Y, halt, W, D), P))
U2_gaga(X, Y, Z, S, P, member_out_gg(p(S, Y, halt, W, D), P)) → turing_out_gaga(t(X, Y, Z), S, P, t(X, Y, Z))
turing_in_gaga(t(X, Y, .(R, L)), S, P, T) → U3_gaga(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U3_gaga(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U4_gaga(X, Y, R, L, S, P, T, turing_in_gaga(t(.(W, X), R, L), S1, P, T))
turing_in_gaga(t(X, Y, []), S, P, T) → U5_gaga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_gaga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_gaga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
turing_in_gaga(t(.(X, L), Y, R), S, P, T) → U7_gaga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_gaga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_gaga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
turing_in_gaga(t([], Y, R), S, P, T) → U9_gaga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_gaga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_gaga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_gaga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_gaga(t([], Y, R), S, P, T)
U8_gaga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_gaga(t(.(X, L), Y, R), S, P, T)
U6_gaga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_gaga(t(X, Y, []), S, P, T)
U4_gaga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_gaga(t(X, Y, .(R, L)), S, P, T)
U4_ggga(X, Y, R, L, S, P, T, turing_out_gaga(t(.(W, X), R, L), S1, P, T)) → turing_out_ggga(t(X, Y, .(R, L)), S, P, T)
turing_in_ggga(t(X, Y, []), S, P, T) → U5_ggga(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_ggga(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → U6_ggga(X, Y, S, P, T, turing_in_gaga(t(.(W, X), space, []), S1, P, T))
U6_ggga(X, Y, S, P, T, turing_out_gaga(t(.(W, X), space, []), S1, P, T)) → turing_out_ggga(t(X, Y, []), S, P, T)
turing_in_ggga(t(.(X, L), Y, R), S, P, T) → U7_ggga(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_ggga(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U8_ggga(X, L, Y, R, S, P, T, turing_in_gaga(t(L, X, .(W, R)), S1, P, T))
U8_ggga(X, L, Y, R, S, P, T, turing_out_gaga(t(L, X, .(W, R)), S1, P, T)) → turing_out_ggga(t(.(X, L), Y, R), S, P, T)
turing_in_ggga(t([], Y, R), S, P, T) → U9_ggga(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U9_ggga(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → U10_ggga(Y, R, S, P, T, turing_in_gaga(t([], space, .(W, R)), S1, P, T))
U10_ggga(Y, R, S, P, T, turing_out_gaga(t([], space, .(W, R)), S1, P, T)) → turing_out_ggga(t([], Y, R), S, P, T)

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U3_GAGA(X, Y, R, L, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), R, L), S1, P, T)
TURING_IN_GAGA(t(X, Y, .(R, L)), S, P, T) → U3_GAGA(X, Y, R, L, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U5_GAGA(X, Y, S, P, T, member_out_gg(p(S, Y, S1, W, r), P)) → TURING_IN_GAGA(t(.(W, X), space, []), S1, P, T)
TURING_IN_GAGA(t([], Y, R), S, P, T) → U9_GAGA(Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))
U7_GAGA(X, L, Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t(L, X, .(W, R)), S1, P, T)
TURING_IN_GAGA(t(X, Y, []), S, P, T) → U5_GAGA(X, Y, S, P, T, member_in_gg(p(S, Y, S1, W, r), P))
U9_GAGA(Y, R, S, P, T, member_out_gg(p(S, Y, S1, W, l), P)) → TURING_IN_GAGA(t([], space, .(W, R)), S1, P, T)
TURING_IN_GAGA(t(.(X, L), Y, R), S, P, T) → U7_GAGA(X, L, Y, R, S, P, T, member_in_gg(p(S, Y, S1, W, l), P))

The TRS R consists of the following rules:

member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U1_gg(X, H, L, member_in_gg(X, L))
U1_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))

The argument filtering Pi contains the following mapping:
t(x1, x2, x3) = t(x1, x3)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
p(x1, x2, x3, x4, x5) = p
.(x1, x2) = .(x2)
member_out_gg(x1, x2) = member_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4) = U1_gg(x1, x3, x4)
[] = []
TURING_IN_GAGA(x1, x2, x3, x4) = TURING_IN_GAGA(x1, x3)
U5_GAGA(x1, x2, x3, x4, x5, x6) = U5_GAGA(x1, x4, x6)
U7_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U7_GAGA(x2, x4, x6, x8)
U3_GAGA(x1, x2, x3, x4, x5, x6, x7, x8) = U3_GAGA(x1, x4, x6, x8)
U9_GAGA(x1, x2, x3, x4, x5, x6) = U9_GAGA(x2, x4, x6)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

TURING_IN_GAGA(t(X, []), P) → U5_GAGA(X, P, member_in_gg(p, P))
U9_GAGA(R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t([], .(R)), P)
TURING_IN_GAGA(t([], R), P) → U9_GAGA(R, P, member_in_gg(p, P))
TURING_IN_GAGA(t(.(L), R), P) → U7_GAGA(L, R, P, member_in_gg(p, P))
U7_GAGA(L, R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(L, .(R)), P)
U5_GAGA(X, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(.(X), []), P)
TURING_IN_GAGA(t(X, .(L)), P) → U3_GAGA(X, L, P, member_in_gg(p, P))
U3_GAGA(X, L, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(.(X), L), P)

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule TURING_IN_GAGA(t(X, .(L)), P) → U3_GAGA(X, L, P, member_in_gg(p, P)) at position [3] we obtained the following new rules:

TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

TURING_IN_GAGA(t(X, []), P) → U5_GAGA(X, P, member_in_gg(p, P))
U9_GAGA(R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t([], .(R)), P)
TURING_IN_GAGA(t([], R), P) → U9_GAGA(R, P, member_in_gg(p, P))
TURING_IN_GAGA(t(.(L), R), P) → U7_GAGA(L, R, P, member_in_gg(p, P))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
U5_GAGA(X, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(.(X), []), P)
U7_GAGA(L, R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(L, .(R)), P)
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
U3_GAGA(X, L, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(.(X), L), P)

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule TURING_IN_GAGA(t([], R), P) → U9_GAGA(R, P, member_in_gg(p, P)) at position [2] we obtained the following new rules:

TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg(p, .(x1)))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

TURING_IN_GAGA(t(X, []), P) → U5_GAGA(X, P, member_in_gg(p, P))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
U9_GAGA(R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t([], .(R)), P)
TURING_IN_GAGA(t(.(L), R), P) → U7_GAGA(L, R, P, member_in_gg(p, P))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
U7_GAGA(L, R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(L, .(R)), P)
U5_GAGA(X, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(.(X), []), P)
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
U3_GAGA(X, L, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(.(X), L), P)

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule TURING_IN_GAGA(t(X, []), P) → U5_GAGA(X, P, member_in_gg(p, P)) at position [2] we obtained the following new rules:

TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U9_GAGA(R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t([], .(R)), P)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(L), R), P) → U7_GAGA(L, R, P, member_in_gg(p, P))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
U5_GAGA(X, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(.(X), []), P)
U7_GAGA(L, R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(L, .(R)), P)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
U3_GAGA(X, L, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(.(X), L), P)

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule TURING_IN_GAGA(t(.(L), R), P) → U7_GAGA(L, R, P, member_in_gg(p, P)) at position [3] we obtained the following new rules:

TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U9_GAGA(R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t([], .(R)), P)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
U5_GAGA(X, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(.(X), []), P)
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
U3_GAGA(X, L, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(.(X), L), P)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
U7_GAGA(L, R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(L, .(R)), P)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U3_GAGA(X, L, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(.(X), L), P) we obtained the following new rules:

U3_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(.(z0), z1), .(z2))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U9_GAGA(R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t([], .(R)), P)
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
U5_GAGA(X, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(.(X), []), P)
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
U3_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
U7_GAGA(L, R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(L, .(R)), P)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U5_GAGA(X, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(.(X), []), P) we obtained the following new rules:

U5_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t(.(z0), []), .(z1))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t(.(z0), []), .(z1))
U9_GAGA(R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t([], .(R)), P)
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
U7_GAGA(L, R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(L, .(R)), P)
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
U3_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U7_GAGA(L, R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t(L, .(R)), P) we obtained the following new rules:

U7_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U9_GAGA(R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t([], .(R)), P)
U5_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t(.(z0), []), .(z1))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
U3_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
U7_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U9_GAGA(R, P, member_out_gg(p, P)) → TURING_IN_GAGA(t([], .(R)), P) we obtained the following new rules:

U9_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t([], .(z0)), .(z1))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t(.(z0), []), .(z1))
U9_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t([], .(z0)), .(z1))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
U3_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
U7_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1))) we obtained the following new rules:

TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(p, z2, member_in_gg(p, z2)))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

                                                          ↳ QDP

                                                            ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t(.(z0), []), .(z1))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
U9_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t([], .(z0)), .(z1))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
U3_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(p, z2, member_in_gg(p, z2)))
U7_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule TURING_IN_GAGA(t([], y0), .(x1)) → U9_GAGA(y0, .(x1), member_out_gg(p, .(x1))) we obtained the following new rules:

TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg(p, .(z2)))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

                                                          ↳ QDP

                                                            ↳ Instantiation

                                                              ↳ QDP

                                                                ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t(.(z0), []), .(z1))
U9_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t([], .(z0)), .(z1))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg(p, .(z2)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
U3_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(p, z2, member_in_gg(p, z2)))
U7_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), member_out_gg(p, .(x1))) we obtained the following new rules:

TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), member_out_gg(p, .(z2)))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

                                                          ↳ QDP

                                                            ↳ Instantiation

                                                              ↳ QDP

                                                                ↳ Instantiation

                                                                  ↳ QDP

                                                                    ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t(.(z0), []), .(z1))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
U9_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t([], .(z0)), .(z1))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg(p, .(z2)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
U3_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(p, z2, member_in_gg(p, z2)))
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), member_out_gg(p, .(z2)))
U7_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule TURING_IN_GAGA(t(y0, []), .(x1)) → U5_GAGA(y0, .(x1), U1_gg(p, x1, member_in_gg(p, x1))) we obtained the following new rules:

TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), U1_gg(p, z2, member_in_gg(p, z2)))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

                                                          ↳ QDP

                                                            ↳ Instantiation

                                                              ↳ QDP

                                                                ↳ Instantiation

                                                                  ↳ QDP

                                                                    ↳ Instantiation

                                                                      ↳ QDP

                                                                        ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t(.(z0), []), .(z1))
U9_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t([], .(z0)), .(z1))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg(p, .(z2)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
U3_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), U1_gg(p, z2, member_in_gg(p, z2)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(p, z2, member_in_gg(p, z2)))
U7_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), member_out_gg(p, .(z2)))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U5_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t(.(z0), []), .(z1)) we obtained the following new rules:

U5_GAGA(.(z0), .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t(.(.(z0)), []), .(z1))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

                                                          ↳ QDP

                                                            ↳ Instantiation

                                                              ↳ QDP

                                                                ↳ Instantiation

                                                                  ↳ QDP

                                                                    ↳ Instantiation

                                                                      ↳ QDP

                                                                        ↳ Instantiation

                                                                          ↳ QDP

                                                                            ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(.(z0), .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t(.(.(z0)), []), .(z1))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
U9_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t([], .(z0)), .(z1))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg(p, .(z2)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
U3_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), U1_gg(p, z2, member_in_gg(p, z2)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(p, z2, member_in_gg(p, z2)))
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), member_out_gg(p, .(z2)))
U7_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U9_GAGA(z0, .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t([], .(z0)), .(z1)) we obtained the following new rules:

U9_GAGA(.(z0), .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t([], .(.(z0))), .(z1))

↳ Prolog

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ Instantiation

                                                  ↳ QDP

                                                    ↳ Instantiation

                                                      ↳ QDP

                                                        ↳ Instantiation

                                                          ↳ QDP

                                                            ↳ Instantiation

                                                              ↳ QDP

                                                                ↳ Instantiation

                                                                  ↳ QDP

                                                                    ↳ Instantiation

                                                                      ↳ QDP

                                                                        ↳ Instantiation

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U5_GAGA(.(z0), .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t(.(.(z0)), []), .(z1))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), U1_gg(p, x1, member_in_gg(p, x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), member_out_gg(p, .(z2)))
TURING_IN_GAGA(t(.(y0), y1), .(x1)) → U7_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
U3_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(.(z0), z1), .(z2))
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), U1_gg(p, z2, member_in_gg(p, z2)))
TURING_IN_GAGA(t(y0, .(y1)), .(x1)) → U3_GAGA(y0, y1, .(x1), member_out_gg(p, .(x1)))
TURING_IN_GAGA(t([], .(z1)), .(z2)) → U9_GAGA(.(z1), .(z2), U1_gg(p, z2, member_in_gg(p, z2)))
U9_GAGA(.(z0), .(z1), member_out_gg(p, .(z1))) → TURING_IN_GAGA(t([], .(.(z0))), .(z1))
U7_GAGA(z0, z1, .(z2), member_out_gg(p, .(z2))) → TURING_IN_GAGA(t(z0, .(z1)), .(z2))
TURING_IN_GAGA(t(.(z0), []), .(z2)) → U5_GAGA(.(z0), .(z2), member_out_gg(p, .(z2)))

The TRS R consists of the following rules:

member_in_gg(H, .(L)) → member_out_gg(H, .(L))
member_in_gg(X, .(L)) → U1_gg(X, L, member_in_gg(X, L))
U1_gg(X, L, member_out_gg(X, L)) → member_out_gg(X, .(L))

The set Q consists of the following terms:

member_in_gg(x0, x1)
U1_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.